Search results for "Automated theorem proving"

showing 2 items of 2 documents

Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle

2018

This paper presents a proof-of-concept application of an approach to system development based on the integration of formal verification and co-simulation. A simple autonomous vehicle has the task of reaching an assigned straight path and then follow it, and it can be controlled by varying its turning speed. The correctness of the proposed control law has been formalized and verified by interactive theorem proving with the Prototype Verification System. Concurrently, the system has been co-simulated using the Prototype Verification System and the MathWorks Simulink tool: The vehicle kinematics have been simulated in Simulink, whereas the controller has been modeled in the logic language of t…

CorrectnessSIMPLE (military communications protocol)Computer scienceProof assistant020207 software engineeringControl engineering02 engineering and technologyFormal methods Software engineering Theorem proving Vehicles Autonomous Vehicles Control laws Integrated simulations Interactive theorem proving Logic languages Proof of concept Prototype verification systems System development020202 computer hardware & architectureAutomated theorem provingSettore ING-INF/04 - AutomaticaControl theory0202 electrical engineering electronic engineering information engineeringPrototype Verification SystemFormal verificationLogic programming
researchProduct

Survey of Formal Verification Methods for Smart Contracts on Blockchain

2019

Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for fo…

Model checkingSmart contractExploitComputer science020206 networking & telecommunications02 engineering and technologyFormal methodsComputer securitycomputer.software_genreSyntax (logic)Automated theorem provingOrder (business)0202 electrical engineering electronic engineering information engineering020201 artificial intelligence & image processingFormal verificationcomputer2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS)
researchProduct